(declare-fun r () String)
(declare-fun s () String)
(declare-fun t () String)
(assert (= s t))
(assert (= (str.indexof s r 1) (str.indexof t r 0)))
(check-sat)
(declare-fun r () String)
(declare-fun s () String)
(declare-fun t () String)
(assert (= s t))
(assert (= (str.indexof s r 0) (str.indexof t r 1)))
(check-sat)
